Linear hybrid automaton is an important type of hybrid systems in the verification of embedded automotive control systems such as in the modeling and analysis of electrical and software architectures and in the robust verification of non-linear chassis control systems via approximation. Current methods for the verification of linear hybrid automata require performing a reachability search computation based on dynamic flow equations. A reachability search computation determines if a certain location is reachable or not, and if a run exists to reach the certain location. If no run exists, then the location is not reachable. However, there are some problems associated with the reachability computation approach such as arithmetic overflow, long computation time, and large memory.
Hybrid systems include both continuous and discrete state variables and they have been widely used as mathematical models for many important applications, such as manufacturing systems, air-traffic management systems, embedded automotive control systems, and real-time communication networks. Most of those applications are safety critical systems and require guarantees of safe operation. Consequently, the formal verification of hybrid systems is important for those safety critical applications.
A linear hybrid automaton is defined by a finite transition graph having nodes identified as locations, and edges identified as discrete transitions in combination with a set V of real variables. Continuous dynamics within each location are subject to a constant polyhedral differential inclusion (also called flow condition), i.e., dynamics of the form φ({right arrow over ({dot over (v)}), where φ is a conjunction of linear constraints over first derivatives of variables in V. Discrete dynamics are modeled by the discrete transitions, each of which has a guard condition and a jump condition over V. A state in a LHA is a pair consisting of a location and a vector of variable values. A set of states is linear if it is definable using a linear predicate for each location, wherein a linear predicate is a set of expressions in a specified form.
For the analysis of LHA, research tools, such as a “HyTech tool disclosed in HyTech: A model checker for hybrid systems”; Software Tools for Technology Transfer, 1:110-122, 1997 by T. Henzinger, P. Ho, and H. Wong-Toi. The heart of HyTech is a procedure that attempts to compute reachable sets, by repeatedly computing successor sets until no new successor states are discovered. While HyTech is used to analyze a number of examples, it suffers from a number of problems as disclosed, for example, in “Some lessons from the HyTech experience”; In Proceedings of the 40th Annual Conference on Decision and Control (CDC), IEE Press, 2001, pp. 2887-2892 by T. Henzinger, J. Preussig, and H. Wong-Toi (hereinafter “HENZINGER”), which includes: (1) the size of reachable state space needed to store reachable sets may exceed available memory; (2) the analysis may require long computation time; (3) for certain LHA the reachable set is not linear and by visiting all reachable states, the HyTech will not terminate; (4) arithmetic overflow may occur because of the limited-precision arithmetic used. Some suggestions for improvement were proposed as disclosed, for example, in HENZINGER. As disclosed, for example, in “PHAVer: Algorithmic Verification of Hybrid Systems past HyTech”; In Proceedings of the Fifth International Workshop on Hybrid Systems: Computation and Control (HSCC), Lecture Notes in Computer Science 3414, Springer-Verlag, 2005, pp. 258-273 by G. Frehse, (hereinafter “FREHSE”), a research tool called PHAVer was developed for analyzing linear hybrid automata. PHAVer overcomes the overflow problem by using robust arithmetic based on the Parma Polyhedra Library (PPL). PHAVer also uses the approach of fixpoint computations over the system state space like HyTech. However, like HyTech, the PHAVer system also suffers from long computation times and large memory consumption for systems with a large number of continuous variables.
Counterexample guided abstraction refinement was used for the verification of hybrid systems as disclosed, for example, in “Abstraction and counterexample-guided refinement in model checking of hybrid systems”; International Journal of Foundations of Computer Science, 14(4):583604, 2003E by Clarke, A. Fehnker, Z. Han, B. Krogh, J. Ouaknine, 0. Stursberg, and M. Theobald., (hereinafter “CLARKE1”) and as disclosed, for example, in “Counter-example guided predicate abstraction of hybrid system”; In TACAS, volume 2619 of LNCS, Springer, 2003 by R. Alur, T. Dang, and F. Ivancic, (hereinafter “ALUR”), where it was for general hybrid systems as disclosed, for example, in CLARKE1 and was for linear dynamic hybrid systems as disclosed, for example, in ALUR. The abstraction models as disclosed, for example, in CLARKE1 and as disclosed, for example, in ALUR involve the state set representation, which was the representation of reachable state set as disclosed, for example, in CLARKE1 and the predicate representation of state set as disclosed, for example, in ALUR. Also the abstraction refinements as disclosed, for example, in CLARKE1 and as disclosed, for example, in ALUR are based on the infeasible prefix of the counterexample.
A concept called locally infeasibility is disclosed in ALUR, which could be viewed as the infeasibility caused by fragments with two transitions, but the general concept of fragment based abstraction refinement is not disclosed in ALUR.
Conventional counterexample fragment based abstraction refinement is applied for general hybrid systems as disclosed, for example, in “Refining Abstractions of Hybrid Systems Using Counterexample Fragments”; In Proceedings of the Fifth International Workshop on Hybrid Systems: Computation and Control (HSCC), Lecture Notes in Computer Science 3414, Springer-Verlag, 2005, pp. 242-257 by A. Fehnker, E. Clarke, S. Jha, B. Krogh, (hereinafter “FEHNKER”). The approach as disclosed, for example, in FEDNKER also involves the state set representation in an abstract model, wherein FEHNKER assumes that a set of fragments is given initially and then it may extend a given fragment later.
As disclosed, for example, in “Verifying Industrial Hybrid Systems with MathSAT”; Electronic Notes in Theoretical Computer Science, Volume 119, Issue 2, 14 Mar. 2005, Pages 17-32 (Proc. BMC 2004, Boston, Mass., Jul. 18, 2004) by G. Audemard, M. Bozzano, A. Cimatti, and R. Sebastiani. (hereinafter “AUDEMARD”), a method based on bounded model checking (BMC) and MathSAT was developed for the bounded reachability analysis of LHA. The method encodes all the paths in the system with lengths up to a certain length bound along with the reachability property into a math-formula, i.e., boolean combinations of boolean variables and linear (in)equalities over real variables. Then MathSAT solver is used to check the satisfiability of the math-formula. If the math-formula is satisfiable, then the reachability property holds; otherwise, the process continues by increasing the length bound and repeating the process until the MathSAT solver terminates or runs out of memory or time. The bounded reachability analysis of LHA cannot prove the unsatisfiability of certain reachability properties, like proving that some bad states can never be reached. The linear hybrid automaton model as disclosed, for example, in AUDEMARD requires that the flow conditions are directly given as constraints on variable value changes for certain time delay, i.e., besides the discrete transitions between different locations there is also a self-loop time elapse transition at each location to represent the variable value changes caused by the time elapses at the location. The above model as disclosed, for example, in AUDEMARD is different from the well known LHA model where the flow conditions are linear constraints over first derivatives of variables; and there is no proof on the equivalence of the above two different models for linear hybrid automaton.
A method of verification of linear hybrid automation (LHA) is needed that transforms an LHA into a linear transition system (LTS) and that uses concurrency for concurrent systems, thereby eliminating the need to perform and store reachable state computations.